0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 17 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 3 ms)
↳20 QDP
↳21 MRRProof (⇔, 37 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
perm1B_in_ga([], []) → perm1B_out_ga([], [])
perm1B_in_ga(.(T27, T28), .(T27, T29)) → U2_ga(T27, T28, T29, perm1B_in_ga(T28, T29))
perm1B_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, selectA_in_aga(T39, T38, X45))
selectA_in_aga(T59, .(T59, T60), T60) → selectA_out_aga(T59, .(T59, T60), T60)
selectA_in_aga(T70, .(T68, T69), .(T68, X78)) → U1_aga(T70, T68, T69, X78, selectA_in_aga(T70, T69, X78))
U1_aga(T70, T68, T69, X78, selectA_out_aga(T70, T69, X78)) → selectA_out_aga(T70, .(T68, T69), .(T68, X78))
U3_ga(T37, T38, T39, T40, selectA_out_aga(T39, T38, X45)) → perm1B_out_ga(.(T37, T38), .(T39, T40))
perm1B_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, perm1B_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, perm1B_out_ga(.(T37, T45), T46)) → perm1B_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T27, T28, T29, perm1B_out_ga(T28, T29)) → perm1B_out_ga(.(T27, T28), .(T27, T29))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
perm1B_in_ga([], []) → perm1B_out_ga([], [])
perm1B_in_ga(.(T27, T28), .(T27, T29)) → U2_ga(T27, T28, T29, perm1B_in_ga(T28, T29))
perm1B_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, selectA_in_aga(T39, T38, X45))
selectA_in_aga(T59, .(T59, T60), T60) → selectA_out_aga(T59, .(T59, T60), T60)
selectA_in_aga(T70, .(T68, T69), .(T68, X78)) → U1_aga(T70, T68, T69, X78, selectA_in_aga(T70, T69, X78))
U1_aga(T70, T68, T69, X78, selectA_out_aga(T70, T69, X78)) → selectA_out_aga(T70, .(T68, T69), .(T68, X78))
U3_ga(T37, T38, T39, T40, selectA_out_aga(T39, T38, X45)) → perm1B_out_ga(.(T37, T38), .(T39, T40))
perm1B_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, perm1B_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, perm1B_out_ga(.(T37, T45), T46)) → perm1B_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T27, T28, T29, perm1B_out_ga(T28, T29)) → perm1B_out_ga(.(T27, T28), .(T27, T29))
PERM1B_IN_GA(.(T27, T28), .(T27, T29)) → U2_GA(T27, T28, T29, perm1B_in_ga(T28, T29))
PERM1B_IN_GA(.(T27, T28), .(T27, T29)) → PERM1B_IN_GA(T28, T29)
PERM1B_IN_GA(.(T37, T38), .(T39, T40)) → U3_GA(T37, T38, T39, T40, selectA_in_aga(T39, T38, X45))
PERM1B_IN_GA(.(T37, T38), .(T39, T40)) → SELECTA_IN_AGA(T39, T38, X45)
SELECTA_IN_AGA(T70, .(T68, T69), .(T68, X78)) → U1_AGA(T70, T68, T69, X78, selectA_in_aga(T70, T69, X78))
SELECTA_IN_AGA(T70, .(T68, T69), .(T68, X78)) → SELECTA_IN_AGA(T70, T69, X78)
PERM1B_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → U5_GA(T37, T38, T39, T46, perm1B_in_ga(.(T37, T45), T46))
U4_GA(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → PERM1B_IN_GA(.(T37, T45), T46)
perm1B_in_ga([], []) → perm1B_out_ga([], [])
perm1B_in_ga(.(T27, T28), .(T27, T29)) → U2_ga(T27, T28, T29, perm1B_in_ga(T28, T29))
perm1B_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, selectA_in_aga(T39, T38, X45))
selectA_in_aga(T59, .(T59, T60), T60) → selectA_out_aga(T59, .(T59, T60), T60)
selectA_in_aga(T70, .(T68, T69), .(T68, X78)) → U1_aga(T70, T68, T69, X78, selectA_in_aga(T70, T69, X78))
U1_aga(T70, T68, T69, X78, selectA_out_aga(T70, T69, X78)) → selectA_out_aga(T70, .(T68, T69), .(T68, X78))
U3_ga(T37, T38, T39, T40, selectA_out_aga(T39, T38, X45)) → perm1B_out_ga(.(T37, T38), .(T39, T40))
perm1B_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, perm1B_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, perm1B_out_ga(.(T37, T45), T46)) → perm1B_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T27, T28, T29, perm1B_out_ga(T28, T29)) → perm1B_out_ga(.(T27, T28), .(T27, T29))
PERM1B_IN_GA(.(T27, T28), .(T27, T29)) → U2_GA(T27, T28, T29, perm1B_in_ga(T28, T29))
PERM1B_IN_GA(.(T27, T28), .(T27, T29)) → PERM1B_IN_GA(T28, T29)
PERM1B_IN_GA(.(T37, T38), .(T39, T40)) → U3_GA(T37, T38, T39, T40, selectA_in_aga(T39, T38, X45))
PERM1B_IN_GA(.(T37, T38), .(T39, T40)) → SELECTA_IN_AGA(T39, T38, X45)
SELECTA_IN_AGA(T70, .(T68, T69), .(T68, X78)) → U1_AGA(T70, T68, T69, X78, selectA_in_aga(T70, T69, X78))
SELECTA_IN_AGA(T70, .(T68, T69), .(T68, X78)) → SELECTA_IN_AGA(T70, T69, X78)
PERM1B_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → U5_GA(T37, T38, T39, T46, perm1B_in_ga(.(T37, T45), T46))
U4_GA(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → PERM1B_IN_GA(.(T37, T45), T46)
perm1B_in_ga([], []) → perm1B_out_ga([], [])
perm1B_in_ga(.(T27, T28), .(T27, T29)) → U2_ga(T27, T28, T29, perm1B_in_ga(T28, T29))
perm1B_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, selectA_in_aga(T39, T38, X45))
selectA_in_aga(T59, .(T59, T60), T60) → selectA_out_aga(T59, .(T59, T60), T60)
selectA_in_aga(T70, .(T68, T69), .(T68, X78)) → U1_aga(T70, T68, T69, X78, selectA_in_aga(T70, T69, X78))
U1_aga(T70, T68, T69, X78, selectA_out_aga(T70, T69, X78)) → selectA_out_aga(T70, .(T68, T69), .(T68, X78))
U3_ga(T37, T38, T39, T40, selectA_out_aga(T39, T38, X45)) → perm1B_out_ga(.(T37, T38), .(T39, T40))
perm1B_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, perm1B_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, perm1B_out_ga(.(T37, T45), T46)) → perm1B_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T27, T28, T29, perm1B_out_ga(T28, T29)) → perm1B_out_ga(.(T27, T28), .(T27, T29))
SELECTA_IN_AGA(T70, .(T68, T69), .(T68, X78)) → SELECTA_IN_AGA(T70, T69, X78)
perm1B_in_ga([], []) → perm1B_out_ga([], [])
perm1B_in_ga(.(T27, T28), .(T27, T29)) → U2_ga(T27, T28, T29, perm1B_in_ga(T28, T29))
perm1B_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, selectA_in_aga(T39, T38, X45))
selectA_in_aga(T59, .(T59, T60), T60) → selectA_out_aga(T59, .(T59, T60), T60)
selectA_in_aga(T70, .(T68, T69), .(T68, X78)) → U1_aga(T70, T68, T69, X78, selectA_in_aga(T70, T69, X78))
U1_aga(T70, T68, T69, X78, selectA_out_aga(T70, T69, X78)) → selectA_out_aga(T70, .(T68, T69), .(T68, X78))
U3_ga(T37, T38, T39, T40, selectA_out_aga(T39, T38, X45)) → perm1B_out_ga(.(T37, T38), .(T39, T40))
perm1B_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, perm1B_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, perm1B_out_ga(.(T37, T45), T46)) → perm1B_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T27, T28, T29, perm1B_out_ga(T28, T29)) → perm1B_out_ga(.(T27, T28), .(T27, T29))
SELECTA_IN_AGA(T70, .(T68, T69), .(T68, X78)) → SELECTA_IN_AGA(T70, T69, X78)
SELECTA_IN_AGA(.(T68, T69)) → SELECTA_IN_AGA(T69)
From the DPs we obtained the following set of size-change graphs:
PERM1B_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → PERM1B_IN_GA(.(T37, T45), T46)
PERM1B_IN_GA(.(T27, T28), .(T27, T29)) → PERM1B_IN_GA(T28, T29)
perm1B_in_ga([], []) → perm1B_out_ga([], [])
perm1B_in_ga(.(T27, T28), .(T27, T29)) → U2_ga(T27, T28, T29, perm1B_in_ga(T28, T29))
perm1B_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, selectA_in_aga(T39, T38, X45))
selectA_in_aga(T59, .(T59, T60), T60) → selectA_out_aga(T59, .(T59, T60), T60)
selectA_in_aga(T70, .(T68, T69), .(T68, X78)) → U1_aga(T70, T68, T69, X78, selectA_in_aga(T70, T69, X78))
U1_aga(T70, T68, T69, X78, selectA_out_aga(T70, T69, X78)) → selectA_out_aga(T70, .(T68, T69), .(T68, X78))
U3_ga(T37, T38, T39, T40, selectA_out_aga(T39, T38, X45)) → perm1B_out_ga(.(T37, T38), .(T39, T40))
perm1B_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, perm1B_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, perm1B_out_ga(.(T37, T45), T46)) → perm1B_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T27, T28, T29, perm1B_out_ga(T28, T29)) → perm1B_out_ga(.(T27, T28), .(T27, T29))
PERM1B_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, selectA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, selectA_out_aga(T39, T38, T45)) → PERM1B_IN_GA(.(T37, T45), T46)
PERM1B_IN_GA(.(T27, T28), .(T27, T29)) → PERM1B_IN_GA(T28, T29)
selectA_in_aga(T59, .(T59, T60), T60) → selectA_out_aga(T59, .(T59, T60), T60)
selectA_in_aga(T70, .(T68, T69), .(T68, X78)) → U1_aga(T70, T68, T69, X78, selectA_in_aga(T70, T69, X78))
U1_aga(T70, T68, T69, X78, selectA_out_aga(T70, T69, X78)) → selectA_out_aga(T70, .(T68, T69), .(T68, X78))
PERM1B_IN_GA(.(T37, T38)) → U4_GA(T37, selectA_in_aga(T38))
U4_GA(T37, selectA_out_aga(T39, T45)) → PERM1B_IN_GA(.(T37, T45))
PERM1B_IN_GA(.(T27, T28)) → PERM1B_IN_GA(T28)
selectA_in_aga(.(T59, T60)) → selectA_out_aga(T59, T60)
selectA_in_aga(.(T68, T69)) → U1_aga(T68, selectA_in_aga(T69))
U1_aga(T68, selectA_out_aga(T70, X78)) → selectA_out_aga(T70, .(T68, X78))
selectA_in_aga(x0)
U1_aga(x0, x1)
PERM1B_IN_GA(.(T37, T38)) → U4_GA(T37, selectA_in_aga(T38))
U4_GA(T37, selectA_out_aga(T39, T45)) → PERM1B_IN_GA(.(T37, T45))
PERM1B_IN_GA(.(T27, T28)) → PERM1B_IN_GA(T28)
selectA_in_aga(.(T59, T60)) → selectA_out_aga(T59, T60)
selectA_in_aga(.(T68, T69)) → U1_aga(T68, selectA_in_aga(T69))
U1_aga(T68, selectA_out_aga(T70, X78)) → selectA_out_aga(T70, .(T68, X78))
PERM1BINGA1 > U4GA2 > selectAinaga1 > U1aga2 > selectAoutaga2 > .2
selectA_in_aga_1=1
PERM1B_IN_GA_1=1
._2=1
selectA_out_aga_2=2
U1_aga_2=1
U4_GA_2=0
selectA_in_aga(x0)
U1_aga(x0, x1)